/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979


␈↓ ↓H␈↓α␈↓ ¬~Midterm Exam: Solutions

␈↓ ↓H␈↓1.[5]  What well known function does the following program compute:

␈↓ ↓H␈↓␈↓ αH␈↓↓foo x ← baz[<x>,␈↓¬NIL␈↓↓]␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓baz[u,v] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ v ␈↓αelse␈↓↓ ␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓         ␈↓αif␈↓↓ ␈↓αat|␈↓↓␈↓αa|␈↓↓u ␈↓αthen␈↓↓ baz[␈↓αd|␈↓↓u,␈↓αa|␈↓↓u . v] ␈↓αelse␈↓↓ ␈↓
␈↓ ↓H␈↓␈↓ αH␈↓↓         baz[␈↓αda|␈↓↓u . [␈↓αaa|␈↓↓u . ␈↓αd|␈↓↓u],v]␈↓

␈↓ ↓H␈↓Solution: ␈↓↓∀x: foo x = fringe x␈↓

␈↓ ↓H␈↓2.[10]␈α∞  Write␈α∞a␈α∂program␈α∞␈↓↓mapbin␈↓␈α∞that␈α∂takes␈α∞three␈α∞arguments:␈α∞a␈α∂binary␈α∞operation,␈α∞␈↓↓F,␈↓␈α∂a␈α∞starting
␈↓ ↓H␈↓␈↓ ↓xvalue␈α
␈↓↓e,␈↓␈αand␈α
a␈α
list␈α␈↓↓u␈↓␈α
 and␈αcombines␈α
the␈α
elements␈αof␈α
the␈αlist␈α
together␈α
with␈α␈↓↓e.␈↓␈α
 If␈αthe␈α
list␈α
is␈αis
␈↓ ↓H␈↓␈↓ ↓xempty,␈α
the␈α
result␈α
is␈α
␈↓↓e,␈↓␈α
if␈α
it␈α
has␈α
on␈α
element␈α
␈↓↓x1␈↓␈α
the␈α
the␈α
result␈α
is␈α
␈↓↓F[x1,e]␈↓,␈α
if␈α
it␈α
is␈α
a␈α
two␈α
element␈α
list
␈↓ ↓H␈↓␈↓ ↓x␈↓↓<x1,x2>␈↓ the result is ␈↓↓F[x1,F[x2,e]]␈↓, etc..  Thus

␈↓ ↓H␈↓␈↓ ∧p␈↓↓mapbin[␈↓¬PLUS␈↓↓,␈↓¬0␈↓↓,␈↓¬(1 2 3 4)␈↓↓]=␈↓¬10␈↓↓.␈↓ 

␈↓ ↓H␈↓Solution:       ␈↓↓mapbin[F,e,u] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ e ␈↓αelse␈↓↓ F[␈↓αa|␈↓↓u,mapbin[F,e,␈↓αd|␈↓↓u]]␈↓

␈↓ ↓H␈↓or in internal form

␈↓ ↓H␈↓¬␈↓ αH(DEFUN MAPBIN (F E U)
␈↓ ↓H␈↓¬␈↓ αH  (COND ((NULL U) E)
␈↓ ↓H␈↓¬␈↓ αH        (T (F (CAR U) (MAPBIN F E (CDR U))))))

␈↓ ↓H␈↓3.[10]␈α  Suppose␈αwe␈αrepresent␈αtwo␈αa␈αdimensional,␈α␈↓↓m␈↓␈αby␈α␈↓↓n,␈↓␈αarray␈αas␈αa␈αlist␈αof␈αlists.␈α Each␈αelement␈αof
␈↓ ↓H␈↓␈↓ ↓xthe␈α⊃main␈α⊃list␈α⊂corresponds␈α⊃to␈α⊃a␈α⊂row␈α⊃in␈α⊃the␈α⊃array␈α⊂and␈α⊃will␈α⊃have␈α⊂␈↓↓n␈↓␈α⊃elements␈α⊃(one␈α⊃for␈α⊂each
␈↓ ↓H␈↓␈↓ ↓xcolumn).␈α The␈αmain␈αlist␈αwill␈αhave␈α␈↓↓m␈↓␈αelements,␈αone␈αfor␈αeach␈αrow.␈α Thus␈αthe␈αelement␈αin␈αthe␈α␈↓↓i␈↓th
␈↓ ↓H␈↓␈↓ ↓xrow␈α
and␈α∞␈↓↓j␈↓th␈α
column␈α∞of␈α
the␈α∞array␈α
is␈α∞the␈α
␈↓↓j␈↓th␈α∞element␈α
of␈α∞the␈α
␈↓↓i␈↓th␈α∞list.␈α
  The␈α∞transpose␈α
of␈α∞a␈α
two
␈↓ ↓H␈↓␈↓ ↓xdimensional␈α␈↓↓m␈↓␈αby␈α
␈↓↓n␈↓␈αarray␈αis␈αan␈α
␈↓↓n␈↓␈αby␈α␈↓↓m␈↓␈αarray␈α
whose␈αcolumns␈αare␈αthe␈α
rows␈αof␈αthe␈αoriginal␈α
(and
␈↓ ↓H␈↓␈↓ ↓xwhose␈α
rows␈αtherefore␈α
are␈α
the␈αcolumns␈α
of␈α
the␈αoriginal).␈α
 Write␈α
a␈αprogram␈α
␈↓↓transpose␈↓␈α
that␈αtakes␈α
a
␈↓ ↓H␈↓␈↓ ↓xlist representing an array and returns the list representing its transpose.  For example

␈↓ ↓H␈↓␈↓ βX␈↓↓transpose ␈↓¬((A B C) (D E F))␈↓↓=␈↓¬((A D) (B E) (C F))␈↓↓.␈↓ 

␈↓ ↓H␈↓Note␈α
that␈α
the␈α
list␈α
representing␈α
the␈α
transpose␈α
of␈α∞an␈α
array␈α
is␈α
the␈α
same␈α
as␈α
the␈α
list␈α∞representing␈α
the
␈↓ ↓H␈↓␈↓ ↓xarray by listing the columns instead of the rows.

␈↓ ↓H␈↓Solution:␈αThe␈αprogram␈α
␈↓↓transpose␈↓␈αstarts␈αby␈αcomputing␈α
the␈αlist␈αof␈αfirst␈α
elements␈αof␈αthe␈αrows␈α
of␈αthe
␈↓ ↓H␈↓␈↓ ↓xtransposed␈α⊂array.␈α⊂ These␈α⊂are␈α⊂just␈α⊂the␈α⊂elements␈α⊃of␈α⊂the␈α⊂first␈α⊂row␈α⊂of␈α⊂the␈α⊂original␈α⊃array,␈α⊂and
␈↓ ↓H␈↓␈↓ ↓x␈↓↓mapcar␈↓␈α⊂does␈α⊂the␈α⊂job.␈α⊂ It␈α∂then␈α⊂calls␈α⊂␈↓↓transp␈↓␈α⊂which␈α⊂goes␈α∂through␈α⊂the␈α⊂remaining␈α⊂rows␈α⊂of␈α∂the
␈↓ ↓H␈↓␈↓ ↓xoriginal␈αarray␈αand␈αfor␈αeach␈α
such␈αrow␈αadds␈αthe␈αelements␈α
to␈αthe␈αend␈αof␈αthe␈α
corresponding␈αnew
␈↓ ↓H␈↓␈↓ ↓xrow␈αthat␈αis␈αbeing␈αconstructed.␈α This␈αis␈αdone␈αby␈αcalling␈α␈↓↓enquel[u,vl]␈↓␈αwhere␈α␈↓↓u␈↓␈αis␈αthe␈αrow␈αof␈αthe
␈↓ ↓H␈↓␈↓ ↓xoriginal array to be processed next and ␈↓↓vl␈↓ is the new list of rows.

␈↓ ↓H␈↓↓␈↓ αxtranspose ul ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓ul ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ transp[␈↓αd|␈↓↓ul, mapcar[[λx: <x>], ␈↓αa|␈↓↓ul]]
␈↓ ↓H␈↓2␈↓ H



␈↓ ↓H␈↓↓␈↓ αxtransp[ul, vl] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓ul ␈↓αthen␈↓↓ vl ␈↓αelse␈↓↓ transp[␈↓αd|␈↓↓ul, enquel[␈↓αa|␈↓↓ul, vl]]

␈↓ ↓H␈↓↓␈↓ αxenquel[u, vl] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ [␈↓αa|␈↓↓vl * <␈↓αa|␈↓↓u>] . enquel[␈↓αd|␈↓↓u, ␈↓αd|␈↓↓vl]

␈↓ ↓H␈↓   or in internal form

␈↓ ↓H␈↓¬␈↓ α((DEFUN TRANSPOSE (UL)
␈↓ ↓H␈↓¬␈↓ α(  (COND ((NULL UL) NIL)
␈↓ ↓H␈↓¬␈↓ α(        (T (TRANSP (CDR UL)
␈↓ ↓H␈↓¬␈↓ α(                   (MAPCAR (FUNCTION (LAMBDA (X) (LIST X)))
␈↓ ↓H␈↓¬␈↓ α(                           (CAR UL))))))
␈↓ ↓H␈↓¬␈↓ α((DEFUN TRANSP (UL VL)
␈↓ ↓H␈↓¬␈↓ α(  (COND ((NULL UL) VL)
␈↓ ↓H␈↓¬␈↓ α(        (T (TRANSP (CDR UL) (ENQUEL (CAR UL) VL)))))

␈↓ ↓H␈↓¬␈↓ α((DEFUN ENQUEL (U VL)
␈↓ ↓H␈↓¬␈↓ α(  (COND ((NULL U) NIL)
␈↓ ↓H␈↓¬␈↓ α(        (T (CONS (APPEND (CAR VL) (LIST (CAR U)))
␈↓ ↓H␈↓¬␈↓ α(                 (ENQUEL (CDR U) (CDR VL))))))

␈↓ ↓H␈↓A␈αsomewhat␈α
more␈αefficient␈α
solution␈αis␈αgiven␈α
by␈α␈↓↓transpos,trans,stackl.␈↓␈α
 They␈αwork␈α
in␈αessentially
␈↓ ↓H␈↓␈↓ ↓xthe␈α
same␈α
way,␈α
but␈α
start␈α
by␈α
reversing␈α
the␈α
the␈α
list␈αof␈α
rows␈α
so␈α
that␈α
the␈α
new␈α
list␈α
of␈α
rows␈α
can␈αbe
␈↓ ↓H␈↓␈↓ ↓xbuilt␈α
by␈αadding␈α
to␈α
the␈αfronts␈α
of␈α
the␈αold␈α
rows␈α
rather␈αthat␈α
to␈α
the␈αend,␈α
thus␈α
avoiding␈αexcessive
␈↓ ↓H␈↓␈↓ ↓xuse of ␈↓↓append.␈↓

␈↓ ↓H␈↓↓␈↓ αxtranspos ul ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓ul ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ [λvl:trans[␈↓αd|␈↓↓vl,mapcar[[λx:<x>],␈↓αa|␈↓↓vl]]][reverse ul]

␈↓ ↓H␈↓↓␈↓ αxtrans[ul, vl] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓ul ␈↓αthen␈↓↓ vl ␈↓αelse␈↓↓ trans[␈↓αd|␈↓↓ul, stackl[␈↓αa|␈↓↓ul, vl]]

␈↓ ↓H␈↓↓␈↓ αxstackl[u, vl] ← ␈↓αif␈↓↓ ␈↓αn|␈↓↓u ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ [␈↓αa|␈↓↓u . ␈↓αa|␈↓↓vl] . stackl[␈↓αd|␈↓↓u, ␈↓αd|␈↓↓vl]

␈↓ ↓H␈↓The internal forms of these programs are:

␈↓ ↓H␈↓¬␈↓ α((DEFUN TRANSPOS (UL)
␈↓ ↓H␈↓¬␈↓ α(  (COND ((NULL UL) NIL)
␈↓ ↓H␈↓¬␈↓ α(        (T ((LAMBDA (VL)
␈↓ ↓H␈↓¬␈↓ α(                (TRANS (CDR VL)
␈↓ ↓H␈↓¬␈↓ α(                       (MAPCAR (FUNCTION (LAMBDA (X) (LIST X)))
␈↓ ↓H␈↓¬␈↓ α(                               (CAR VL))))
␈↓ ↓H␈↓¬␈↓ α(            (REVERSE UL)) )))

␈↓ ↓H␈↓¬␈↓ α((DEFUN TRANS (UL VL)
␈↓ ↓H␈↓¬␈↓ α(  (COND ((NULL UL) VL)
␈↓ ↓H␈↓¬␈↓ α(        (T (TRANS (CDR UL) (STACKL (CAR UL) VL)))))

␈↓ ↓H␈↓¬␈↓ α((DEFUN STACKL (U VL)
␈↓ ↓H␈↓¬␈↓ α(  (COND ((NULL U) NIL)
␈↓ ↓H␈↓¬␈↓ α(        (T (CONS (CONS (CAR U) (CAR VL)) (STACKL (CDR U) (CDR VL))))))

␈↓ ↓H␈↓A third solution given by many students is:

␈↓ ↓H␈↓␈↓ α3␈↓↓transpose u←␈↓αif␈↓↓ [␈↓αn|␈↓↓u qor ␈↓αn|␈↓↓␈↓αa|␈↓↓u] ␈↓αthen␈↓↓ ␈↓¬NIL␈↓↓ ␈↓αelse␈↓↓ mapcar[␈↓αa␈↓↓, u] . transpose mapcar[␈↓αd␈↓↓,u]␈↓ 
␈↓ ↓H␈↓␈↓ 93


␈↓ ↓H␈↓which has the internal form

␈↓ ↓H␈↓¬␈↓ α((DEFUN TRANSPOSE (U)
␈↓ ↓H␈↓¬␈↓ α(  (COND ((OR (NULL U) (NULL (CAR U))) NIL)
␈↓ ↓H␈↓¬␈↓ α(        (T (CONS (MAPCAR (FUNCTION CAR) U)
␈↓ ↓H␈↓¬␈↓ α(                 (TRANSPOSE (MAPCAR (FUNCTION CDR) U))))))

␈↓ ↓H␈↓4.[20]␈α
 Suppose␈α
a␈αset␈α
of␈α
cities,␈α
represented␈αby␈α
the␈α
list␈α
␈↓↓CITIES,␈↓␈αare␈α
interconnected␈α
by␈αrailroads.␈α
We
␈↓ ↓H␈↓␈↓ ↓xuse␈α⊃the␈α⊂edge␈α⊃representation␈α⊃of␈α⊂graphs␈α⊃from␈α⊃problem␈α⊂4␈α⊃of␈α⊃the␈α⊂homework␈α⊃to␈α⊃represent␈α⊂the
␈↓ ↓H␈↓␈↓ ↓xshipping␈αneeds␈αof␈αthese␈αcities.␈α Thus␈αthe␈αedge␈α␈↓¬(A␈αB␈α6)␈↓␈αindicates␈αthat␈α␈↓¬6␈α␈↓tons␈αof␈αgoods␈αmust␈αbe
␈↓ ↓H␈↓␈↓ ↓xshipped␈αfrom␈α
city␈α␈↓¬A␈α
␈↓to␈αcity␈α
␈↓¬B,␈α␈↓i.e.␈α
they␈αwill␈α
be␈αpicked␈α
up␈αat␈α
␈↓¬A␈α␈↓and␈α
unloaded␈αat␈α
␈↓¬B.␈α␈↓␈α
Call␈αthis
␈↓ ↓H␈↓␈↓ ↓xgraph␈α∂ ␈↓↓FREIGHT.␈↓␈α∂ Someone␈α∂at␈α∂the␈α∂railroad␈α∂chooses␈α∂a␈α∂route␈α∂for␈α∂the␈α∂train␈α∂to␈α∂follow.␈α∞This
␈↓ ↓H␈↓␈↓ ↓xroute␈α∞is␈α∞represented␈α∞by␈α∞a␈α∞list␈α∞of␈α∞cities␈α∞in␈α∞the␈α
order␈α∞they␈α∞are␈α∞visited,␈α∞e.g.␈α∞␈↓¬(A␈α∞B␈α∞C)␈↓.␈α∞No␈α∞city␈α
is
␈↓ ↓H␈↓␈↓ ↓xvisted␈αmore␈αthan␈αonce.␈αWhile␈αtravelling␈αthis␈αroute,␈αthe␈αtrain␈αwill␈αpick␈αup␈αall␈αgoods␈αwhich␈αare
␈↓ ↓H␈↓␈↓ ↓xto␈αbe␈αdelivered␈αto␈αany␈αcity␈αappearing␈αlater␈αin␈αthe␈αroute.␈α Write␈αa␈αprogram␈α␈↓↓pickup␈↓␈αwhich␈αtakes
␈↓ ↓H␈↓␈↓ ↓xthe␈α
graph␈α∞␈↓↓FREIGHT␈↓␈α
and␈α∞a␈α
route␈α
␈↓↓ROUTE,␈↓␈α∞and␈α
a␈α∞city␈α
␈↓↓CITY,␈↓␈α
appearing␈α∞in␈α
the␈α∞route,␈α
and
␈↓ ↓H␈↓␈↓ ↓xreturns␈α
a␈α
list␈α
of␈α
the␈α
form␈α
␈↓¬((city␈α∞number)␈α
...)␈↓␈α
which␈α
describes␈α
how␈α
much␈α
freight␈α
is␈α∞to␈α
be
␈↓ ↓H␈↓␈↓ ↓xpicked␈αup␈αat␈α␈↓↓CITY␈↓␈αand␈αfor␈αwhat␈αdestinations.␈α Thus␈α␈↓¬(B␈α4)␈↓␈αmeans␈αpick␈αup␈α␈↓¬4␈α␈↓tons␈αto␈αgo␈αto␈α␈↓¬B.␈α␈↓
␈↓ ↓H␈↓␈↓ ↓xWrite␈α
similar␈α
program,␈α
␈↓↓drop,␈↓␈αwhich␈α
returns␈α
a␈α
list␈α
of␈αthe␈α
same␈α
form,␈α
describing␈α
how␈αmany␈α
tons
␈↓ ↓H␈↓␈↓ ↓xare␈αto␈α
be␈αdropped␈αat␈α
␈↓↓CITY,␈↓␈αand␈α
where␈αthey␈αcame␈α
from.␈α The␈αrailraod␈α
has␈αthe␈α
problem␈αthat
␈↓ ↓H␈↓␈↓ ↓xthe␈αtrain␈αhas␈αa␈αmaximum␈αcapacity␈αof␈α
␈↓↓FULL␈↓␈αtons.␈α Using␈α␈↓↓pickup␈↓␈αand␈α␈↓↓drop,␈↓␈αwrite␈α
a␈αprogram
␈↓ ↓H␈↓␈↓ ↓x␈↓↓loadcheck␈↓␈αthat␈αreturns␈α␈↓¬OVERLOAD␈α␈↓␈α
if␈αthe␈αtrain␈αwill␈αever␈αhave␈α
to␈αcarry␈αmore␈αthan␈α␈↓↓FULL␈↓␈αtons␈α
as
␈↓ ↓H␈↓␈↓ ↓xit goes along ␈↓↓ROUTE␈↓ and returns ␈↓¬OK ␈↓otherwise.

␈↓ ↓H␈↓Solution:␈α
First␈α
of␈α
all,␈α
it␈α
is␈α
important␈αto␈α
determine␈α
which␈α
cities␈α
precede␈α
of␈α
follow␈α
CITY␈αin␈α
ROUTE.
␈↓ ↓H␈↓␈↓ ↓xFIND-GOOD-CITIES␈α
finds␈α
the␈α∞cities␈α
following␈α
CITY␈α∞in␈α
ROUTE.␈α
 By␈α∞reversing␈α
ROUTE
␈↓ ↓H␈↓␈↓ ↓xwe␈αuse␈αit␈αto␈αfind␈αthe␈αcities␈αpreceding␈αto␈αCITY␈αin␈αROUTE.␈α We␈αuse␈αthe␈αcities␈αfollowing␈αCITY
␈↓ ↓H␈↓␈↓ ↓xin␈α∞PICKUP,␈α∞and␈α∞the␈α∞cities␈α∞preceding␈α∞in␈α∞DROP.␈α∞ Having␈α∞got␈α∞these␈α∞cities,␈α∞calling␈α∞the␈α∂list␈α∞of
␈↓ ↓H␈↓␈↓ ↓xthem␈α⊂GOOD-CITIES,␈α⊃we␈α⊂now␈α⊂map␈α⊃through␈α⊂FREIGHT,␈α⊂looking␈α⊃for␈α⊂edges␈α⊂of␈α⊃the␈α⊂correct
␈↓ ↓H␈↓␈↓ ↓xform,␈αi.e.,␈α
one␈αcity␈α
is␈αCITY,␈α
the␈αother␈αis␈α
in␈αGOOD-CITIES.␈α
 (The␈αdesired␈α
order␈αis␈αopposite␈α
in
␈↓ ↓H␈↓␈↓ ↓xPICKUP␈α∞and␈α∞DROP.)␈α∞We␈α∞use␈α∞MAP-APPEND,␈α
which␈α∞was␈α∞defined␈α∞in␈α∞the␈α∞solutions␈α∞of␈α
the
␈↓ ↓H␈↓␈↓ ↓xfirst homework; there are a variety of ways to achieve the same effect.

␈↓ ↓H␈↓To␈αdo␈αLOADCHECK␈α
we␈αneed␈αto␈α
keep␈αtrack␈αof␈α
the␈αload␈αbeing␈α
carried␈αas␈αthe␈α
train␈αgoes␈αfrom␈α
city
␈↓ ↓H␈↓␈↓ ↓xto␈αcity␈αalong␈αroute.␈αWe␈αuse␈αthe␈αprogram␈αLC,␈αwhich␈αhas␈αa␈αvariable␈αfor␈αthis,␈αinitialized␈αto␈α0.␈αAt
␈↓ ↓H␈↓␈↓ ↓xeach␈αcity␈αwe␈αcompute␈αthe␈αchange␈αin␈αthe␈αload␈αby␈αtotalling␈αup␈αwhat␈αis␈αpicked␈αup␈αand␈αdropped.
␈↓ ↓H␈↓␈↓ ↓xWe check the new total against FULL.

␈↓ ↓H␈↓↓        pickup[city, route, freight] ← 
␈↓ ↓H␈↓↓            {find-good-cities[city, route]}[λgood-cities: 
␈↓ ↓H␈↓↓                map-append[
␈↓ ↓H␈↓↓                    [λx: ␈↓αif␈↓↓ ␈↓αa|␈↓↓x = city ∧ ␈↓αad|␈↓↓x ε good-cities ␈↓αthen␈↓↓ <␈↓αd|␈↓↓x>], 
␈↓ ↓H␈↓↓                    freight]]
␈↓ ↓H␈↓4␈↓ H



␈↓ ↓H␈↓↓        drop[city, route, freight] ← 
␈↓ ↓H␈↓↓            {find-good-cities[city, reverse route]}[λgood-cities: 
␈↓ ↓H␈↓↓                map-append[
␈↓ ↓H␈↓↓                    [λx: ␈↓αif␈↓↓ ␈↓αad|␈↓↓x = city ∧ ␈↓αa|␈↓↓x ε good-cities ␈↓αthen␈↓↓ 
␈↓ ↓H␈↓↓                           <<␈↓αa|␈↓↓x, ␈↓αadd|␈↓↓x>>], 
␈↓ ↓H␈↓↓                    freight]]


␈↓ ↓H␈↓↓        find-good-cities[city, route] ← 
␈↓ ↓H␈↓↓            ␈↓αif␈↓↓ ␈↓αn|␈↓↓route ␈↓αthen␈↓↓ ␈↓¬ERROR-I-THOUGHT-YOU-SAID-CITY-WAS-IN-ROUTE!␈↓↓
␈↓ ↓H␈↓↓            ␈↓αelse␈↓↓ ␈↓αif␈↓↓ ␈↓αa|␈↓↓route = city ␈↓αthen␈↓↓ ␈↓αd|␈↓↓route
␈↓ ↓H␈↓↓            ␈↓αelse␈↓↓ find-good-cities[city, ␈↓αd|␈↓↓route]


␈↓ ↓H␈↓↓        loadcheck[route, freight] ← lc[route, freight, 0]

␈↓ ↓H␈↓↓        lc[route, freight, load] ← 
␈↓ ↓H␈↓↓            ␈↓αif␈↓↓ ␈↓αn|␈↓↓route ␈↓αthen␈↓↓ ␈↓¬OK␈↓↓
␈↓ ↓H␈↓↓            ␈↓αelse␈↓↓ apply [
␈↓ ↓H␈↓↓                [λp, d: ␈↓αif␈↓↓ load + p + -d > full ␈↓αthen␈↓↓ ␈↓¬OVERLOAD␈↓↓
␈↓ ↓H␈↓↓                        ␈↓αelse␈↓↓ lc[␈↓αd|␈↓↓route, freight, load + p + -d]], 
␈↓ ↓H␈↓↓                total pickup[␈↓αa|␈↓↓route, route, freight], 
␈↓ ↓H␈↓↓                total drop[␈↓αa|␈↓↓route, route, freight]]

␈↓ ↓H␈↓↓        total info ← apply[␈↓¬PLUS␈↓↓, mapcar[␈↓¬CADR␈↓↓, info]]


␈↓ ↓H␈↓or in internal form

␈↓ ↓H␈↓¬␈↓ ↓h(DEFUN PICKUP (CITY ROUTE FREIGHT)
␈↓ ↓H␈↓¬␈↓ ↓h       ((LAMBDA (GOOD-CITIES)
␈↓ ↓H␈↓¬␈↓ ↓h                (MAP-APPEND
␈↓ ↓H␈↓¬␈↓ ↓h                 (FUNCTION (LAMBDA (X)
␈↓ ↓H␈↓¬␈↓ ↓h                                   (COND  ((AND (EQ (CAR X) CITY)
␈↓ ↓H␈↓¬␈↓ ↓h                                                (MEMBER (CADR X) GOOD-CITIES))
␈↓ ↓H␈↓¬␈↓ ↓h                                           (LIST (CDR X))))))
␈↓ ↓H␈↓¬␈↓ ↓h                 FREIGHT))
␈↓ ↓H␈↓¬␈↓ ↓h        (FIND-GOOD-CITIES CITY ROUTE)))

␈↓ ↓H␈↓¬␈↓ ↓h(DEFUN DROP (CITY ROUTE FREIGHT)
␈↓ ↓H␈↓¬␈↓ ↓h       ((LAMBDA (GOOD-CITIES)
␈↓ ↓H␈↓¬␈↓ ↓h                (MAP-APPEND
␈↓ ↓H␈↓¬␈↓ ↓h                 (FUNCTION (LAMBDA (X)
␈↓ ↓H␈↓¬␈↓ ↓h                                   (COND  ((AND (EQ (CADR X) CITY)
␈↓ ↓H␈↓¬␈↓ ↓h                                                (MEMBER (CAR X) GOOD-CITIES))
␈↓ ↓H␈↓¬␈↓ ↓h                                           (LIST (LIST (CAR X) (CADDR X)))))))
␈↓ ↓H␈↓¬␈↓ ↓h                 FREIGHT))
␈↓ ↓H␈↓¬␈↓ ↓h        (FIND-GOOD-CITIES CITY (REVERSE ROUTE))))
␈↓ ↓H␈↓␈↓ 95



␈↓ ↓H␈↓¬␈↓ ↓h(DEFUN FIND-GOOD-CITIES (CITY ROUTE)
␈↓ ↓H␈↓¬␈↓ ↓h       (COND ((NULL ROUTE) 'ERROR-I-THOUGHT-YOU-SAID-CITY-WAS-IN-ROUTE!)
␈↓ ↓H␈↓¬␈↓ ↓h             ((EQ (CAR ROUTE) CITY) (CDR ROUTE))
␈↓ ↓H␈↓¬␈↓ ↓h             (T (FIND-GOOD-CITIES CITY (CDR ROUTE)))))


␈↓ ↓H␈↓¬␈↓ ↓h(DEFUN LOADCHECK (ROUTE FREIGHT)
␈↓ ↓H␈↓¬␈↓ ↓h       (LC ROUTE FREIGHT 0))


␈↓ ↓H␈↓¬␈↓ ↓h(DEFUN LC (ROUTE FREIGHT LOAD)
␈↓ ↓H␈↓¬␈↓ ↓h   (COND ((NULL ROUTE) 'OK)
␈↓ ↓H␈↓¬␈↓ ↓h         (T ((FUNCTION
␈↓ ↓H␈↓¬␈↓ ↓h                (LAMBDA (P D)
␈↓ ↓H␈↓¬␈↓ ↓h                   (COND ((GREATERP (PLUS LOAD P (MINUS D)) FULL)
␈↓ ↓H␈↓¬␈↓ ↓h                          'OVERLOAD)
␈↓ ↓H␈↓¬␈↓ ↓h                         (T (LC (CDR ROUTE)
␈↓ ↓H␈↓¬␈↓ ↓h                                FREIGHT
␈↓ ↓H␈↓¬␈↓ ↓h                                (PLUS LOAD P (MINUS D)))))))
␈↓ ↓H␈↓¬␈↓ ↓h                 (TOTAL (PICKUP (CAR ROUTE) ROUTE FREIGHT))
␈↓ ↓H␈↓¬␈↓ ↓h                 (TOTAL (DROP (CAR ROUTE) ROUTE FREIGHT))))))

␈↓ ↓H␈↓¬␈↓ ↓h(DEFUN TOTAL (INFO)
␈↓ ↓H␈↓¬␈↓ ↓h       (APPLY 'PLUS (MAPCAR 'CADR INFO)))


␈↓ ↓H␈↓5.[5]  Give statements expressing the following facts

␈↓ ↓H␈↓␈↓ αλ5.1. ␈↓↓revers␈↓ing a list does not change its ␈↓↓length.␈↓

␈↓ ↓H␈↓␈↓ αλSolution: ␈↓↓∀u:length reverse u=length u.␈↓

␈↓ ↓H␈↓␈↓ αλ5.2.␈α∞ ␈↓↓append␈↓ing␈α∞a␈α∞single␈α∞element␈α∞list␈α∞onto␈α∞a␈α
second␈α∞list␈α∞is␈α∞the␈α∞same␈α∞as␈α∞␈↓↓cons␈↓ing␈α∞that␈α
element
␈↓ ↓H␈↓␈↓ αλonto the second list.

␈↓ ↓H␈↓␈↓ αλSolution: ␈↓↓∀x v: <x>*v = [x . v]␈↓

␈↓ ↓H␈↓␈↓ αλAlternate solution: ␈↓↓∀u v: [length u = 1 ⊃ u*v = [␈↓αa|␈↓↓u . v] ]␈↓